(*----
  Name: changes.mli
  Copyright M Wahab 2010-2014
  Author: M Wahab  <mwb.cde@gmail.com>

  This file is part of HSeq

  HSeq is free software; you can redistribute it and/or modify it under
  the terms of the Lesser GNU General Public License as published by
  the Free Software Foundation; either version 3, or (at your option)
  any later version.

  HSeq is distributed in the hope that it will be useful, but WITHOUT
  ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
  FITNESS FOR A PARTICULAR PURPOSE.  See the Lesser GNU General Public
  License for more details.

  You should have received a copy of the Lesser GNU General Public
  License along with HSeq.  If not see <http://www.gnu.org/licenses/>.
  ----*)

(** The changes made to a goal by a tactic are recorded as data
    embedded in the goal. A tactic can access the data by reading the
    [changes] field of the goal.
*)

(**
   The record holding information generated by tactics.
*)
type t = 
    { 
      goal_tags:Tag.t list; 
      (** new sub-goals produced by the tactic. *) 
      asm_tags: Tag.t list;
      (** new assumption produced by the tactic. *)
      cncl_tags: Tag.t list;
      (** new conclusions produced by the tactic. *)
      term_list: Basic.term list
    (** new constants produced by the tactic. *)
    }

(** Make an empty changes record. *)
val empty: unit -> t

(** Accessors *)
val dest: t -> (Tag.t list * Tag.t list * Tag.t list * Basic.term list)
val goals: t -> Tag.t list
val aforms: t -> Tag.t list
val cforms: t -> Tag.t list
val terms: t -> Basic.term list

(** Construct a record of goal changes. *)
val make:
  Tag.t list -> Tag.t list -> Tag.t list -> Basic.term list -> t

(** [add chngs gs hs cs ts]: Append [gs], [hs], [cs] and [ts] to
    [r.goals], [r.aforms], [r.cforms] and [r.terms] respectively.  *)
val add: 
  t -> Tag.t list -> Tag.t list -> Tag.t list -> Basic.term list 
  -> t

(** [rev_append l r]: Reverse-append the fields of [l] to [r]. *)
val rev_append: t -> t -> t

(** [rev l]: Reverse the contents of the fields of [l]. *)
val rev: t -> t

(** [combine l r]: Do [rev_append (rev l) r]. *)
val combine: t -> t -> t

(** [flatten l]: flatten the list of changes [l]. *)
val flatten: t list -> t

(** [add_goals: inf l]: Add list [l] to the goals of [inf] *)
val add_goals: t -> Tag.t list -> t
(** [add_aforms: inf l]: Add list [l] to the assumptions of [inf] *)
val add_aforms: t -> Tag.t list -> t
(** [add_cforms: inf l]: Add list [l] to the conclusions of [inf] *)
val add_cforms: t -> Tag.t list -> t
(** [add_terms: inf l]: Add list [l] to the constants of [inf] *)
val add_terms: t -> Basic.term list -> t
